$\forall$$l$:IdLnk, ${\it dt}$:${\it tg}$:Id fp$\rightarrow$ Type, ${\it knd}$:Knd, $T$:Type.
\\[0ex](($\uparrow$isrcv(${\it knd}$)) $\Rightarrow$ (lnk(${\it knd}$) = $l$) $\Rightarrow$ ($T$ = ${\it dt}$(tag(${\it knd}$))?Void)) $\Rightarrow$ lnk{-}decl($l$;${\it dt}$) $\parallel$ ${\it knd}$ : $T$